Search Results

Documents authored by Feng, Yuan

Document
DOI: 10.4230/LIPIcs.CONCUR.2017.35
Model Checking Omega-regular Properties for Quantum Markov Chains

Authors: Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.
Cite as

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying. Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{feng_et_al:LIPIcs.CONCUR.2017.35,
  author =	{Feng, Yuan and Hahn, Ernst Moritz and Turrini, Andrea and Ying, Shenggang},
  title =	{{Model Checking Omega-regular Properties for Quantum Markov Chains}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.35},
  URN =		{urn:nbn:de:0030-drops-77818},
  doi =		{10.4230/LIPIcs.CONCUR.2017.35},
  annote =	{Keywords: Quantum Markov chains, model checking, omega-regular properties, bottom strongly connected component}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.427
On Coinduction and Quantum Lambda Calculi

Authors: Yuxin Deng, Yuan Feng, and Ugo Dal Lago

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.
Cite as

Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 427-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{deng_et_al:LIPIcs.CONCUR.2015.427,
  author =	{Deng, Yuxin and Feng, Yuan and Dal Lago, Ugo},
  title =	{{On Coinduction and Quantum Lambda Calculi}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{427--440},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.427},
  URN =		{urn:nbn:de:0030-drops-53883},
  doi =		{10.4230/LIPIcs.CONCUR.2015.427},
  annote =	{Keywords: Quantum lambda calculi, contextual equivalence, bisimulation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.441
Toward Automatic Verification of Quantum Cryptographic Protocols

Authors: Yuan Feng and Mingsheng Ying

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.
Cite as

Yuan Feng and Mingsheng Ying. Toward Automatic Verification of Quantum Cryptographic Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 441-455, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{feng_et_al:LIPIcs.CONCUR.2015.441,
  author =	{Feng, Yuan and Ying, Mingsheng},
  title =	{{Toward Automatic Verification of Quantum Cryptographic Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{441--455},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.441},
  URN =		{urn:nbn:de:0030-drops-53936},
  doi =		{10.4230/LIPIcs.CONCUR.2015.441},
  annote =	{Keywords: Quantum cryptographic protocols, Verification, Bisimulation, Security}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact